Nuprl Lemma : random_wf
11,40
postcript
pdf
p
:finite-prob-space,
a
,
b
:atom{2:n}. random{2:n}(
p
;
a
;
b
)
p-outcome(
p
)
latex
Definitions
finite-prob-space
,
t
T
,
atom{$n:n}
,
random{$n:n}(
p
;
a
;
b
)
,
,
p-outcome(
p
)
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
Lemmas
finite-prob-space
wf
origin
p:finite-prob-space, a,b:atom{2:n}. random{2:n}(p; a; b) 
p-outcome(p) p:finite-prob-space, a,b:atom{2:n}. random{2:n}(p; a; b) p-outcome(p) TB(x)x:A. B(x)